|
Transaction Logic is an extension of predicate logic that accounts in a clean and declarative way for the phenomenon of state changes in logic programs and databases. This extension adds connectives specifically designed for combining simple actions into complex transactions and for providing control over their execution. The logic has a natural model theory and a sound and complete proof theory. Transaction Logic has a Horn clause subset, which has a procedural as well as a declarative semantics. The important features of the logic include hypothetical and committed updates, dynamic constraints on transaction execution, non-determinism, and bulk updates. In this way, Transaction Logic is able to declaratively capture a number of non-logical phenomena, including procedural knowledge in artificial intelligence, active databases, and methods with side effects in object databases. Transaction Logic was originally proposed in 〔A.J. Bonner and M. Kifer (1993), ''Transaction Logic Programming'', International Conference on Logic Programming (ICLP), 1993.〕 by (Anthony Bonner ) and (Michael Kifer ) and later described in more detail in 〔A.J. Bonner and M. Kifer (1994), ''An Overview of Transaction Logic'', Theoretical Computer Science, 133:2, 1994.〕 and.〔A.J. Bonner and M. Kifer (1998), (''Logic Programming for Database Transactions'' ) in Logics for Databases and Information Systems, J. Chomicki and G. Saake (eds.), Kluwer Academic Publ., 1998.〕 The most comprehensive description appears in.〔A.J. Bonner and M. Kifer (1995), (''Transaction Logic Programming (or A Logic of Declarative and Procedural Knowledge)'' ). Technical Report CSRI-323, November 1995, Computer Science Research Institute, University of Toronto.〕 In later years, Transaction Logic was extended in various ways, including concurrency,〔A.J. Bonner and M. Kifer (1996), (''Concurrency and communication in Transaction Logic'' ), Joint Intl. Conference and Symposium on Logic Programming, Bonn, Germany, September 1996〕 defeasible reasoning,〔P. Fodor and M. Kifer (2011), (''Transaction Logic with Defaults and Argumentation Theories'' ). In Technical communications of the 27th International Conference on Logic Programming (ICLP), July 2011.〕 partially defined actions,〔M. Rezk and M. Kifer (2012), (''Transaction Logic with Partially Defined Actions'' ). Journal on Data Semantics, August 2012, vol. 1, no. 2, Springer.〕 and other features.〔H. Davulcu, M. Kifer and I.V. Ramakrishnan (2004), (CTR-S: A Logic for Specifying Contracts in Semantic Web Services'' ). Proceedings of the 13-th World Wide Web Conference (WWW2004), May 2004.〕〔P. Fodor and M. Kifer (2010), (''Tabling for Transaction Logic'' ). In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), July 2010.〕 In 2013, the original paper on Transaction Logic 〔 has won the 20-year Test of Time Award as the most influential paper from the proceedings of (ICLP 1993 conference ) in the preceding 20 years. == Examples == Graph coloring. Here tinsert denotes the elementary update operation of ''transactional insert''. The connective ⊗ is called ''serial conjunction''. colorNode <- // color one node correctly node(N) ⊗ &neg; colored(N,_) ⊗ color(C) ⊗ ¬(adjacent(N,N2) ∧ colored(N2,C)) ⊗ tinsert(colored(N,C)). colorGraph <- ¬uncoloredNodesLeft. colorGraph <- colorNode ⊗ colorGraph. Pyramid stacking. The elementary update tdelete represents the ''transactional delete'' operation. stack(N,X) <- N>0 ⊗ move(Y,X) ⊗ stack(N-1,Y). stack(0,X). move(X,Y) <- pickup(X) ⊗ putdown(X,Y). pickup(X) <- clear(X) ⊗ on(X,Y) ⊗ ⊗ tdelete(on(X,Y)) ⊗ tinsert(clear(Y)). putdown(X,Y) <- wider(Y,X) ⊗ clear(Y) ⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)). Hypothetical execution. Here <> is the modal operator of possibility: If both action1 and action2 are possible, execute action1. Otherwise, if only action2 is possible, then execute it. execute <- <>action1 ⊗ <>action2 ⊗ action1. execute <- ¬<>action1 ⊗ <>action2 ⊗ action2. Dining philosophers. Here | is the logical connective of parallel conjunction of Concurrent Transaction Logic.〔 diningPhilosophers <- phil(1) | phil(2) | phil(3) | phil(4). 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Transaction logic」の詳細全文を読む スポンサード リンク
|